A:Dsys, i, a:Id. a declared in M(i)  Prop 

latex

Definitions	Dsys, t  T, Id, x:A. B(x), Valtype(da;k), a declared in M, P  Q, M(i), MsgA, Knd, x. t(x), a:A fp B(a), locl(a), KindDeq, x  dom(f), b, Prop
Lemmas	assert wf, fpf-dom wf, Kind-deq wf, locl wf, fpf-trivial-subtype-top, Knd wf, d-m wf, msga wf, Id wf, dsys wf